open HolKernel Parse boolLib bossLib wordsLib;

val _ = new_theory "MARS_Sbox";

val Sbox_def = Define`
  Sbox i = case i : word32 of
    0x0w => 0x9D0C479w  | 0x1w => 0x28C8FFE0w | 0x2w => 0x84AA6C39w
  | 0x3w => 0x9DAD7287w | 0x4w => 0x7DFF9BE3w | 0x5w => 0xD4268361w
  | 0x6w => 0xC96DA1D4w | 0x7w => 0x7974CC93w | 0x8w => 0x85D0582Ew
  | 0x9w => 0x2A4B5705w | 0xAw => 0x1CA16A62w | 0xBw => 0xC3BD279Dw
  | 0xCw => 0xF1F25E5w  | 0xDw => 0x5160372Fw | 0xEw => 0xC695C1FBw
  | 0xFw => 0x4D7FF1E4w | 0x10w => 0xAE5F6BF4w | 0x11w => 0xD72EE46w
  | 0x12w => 0xFF23DE8Aw | 0x13w => 0xB1CF8E83w | 0x14w => 0xF14902E2w
  | 0x15w => 0x3E981E42w | 0x16w => 0x8BF53EB6w | 0x17w => 0x7F4BF8ACw
  | 0x18w => 0x83631F83w | 0x19w => 0x25970205w | 0x1Aw => 0x76AFE784w
  | 0x1Bw => 0x3A7931D4w | 0x1Cw => 0x4F846450w | 0x1Dw => 0x5C64C3F6w
  | 0x1Ew => 0x210A5F18w | 0x1Fw => 0xC6986A26w | 0x20w => 0x28F4E826w
  | 0x21w => 0x3A60A81Cw | 0x22w => 0xD340A664w | 0x23w => 0x7EA820C4w
  | 0x24w => 0x526687C5w | 0x25w => 0x7EDDD12Bw | 0x26w => 0x32A11D1Dw
  | 0x27w => 0x9C9EF086w | 0x28w => 0x80F6E831w | 0x29w => 0xAB6F04ADw
  | 0x2Aw => 0x56FB9B53w | 0x2Bw => 0x8B2E095Cw | 0x2Cw => 0xB68556AEw
  | 0x2Dw => 0xD2250B0Dw | 0x2Ew => 0x294A7721w | 0x2Fw => 0xE21FB253w
  | 0x30w => 0xAE136749w | 0x31w => 0xE82AAE86w | 0x32w => 0x93365104w
  | 0x33w => 0x99404A66w | 0x34w => 0x78A784DCw | 0x35w => 0xB69BA84Bw
  | 0x36w => 0x4046793w  | 0x37w => 0x23DB5C1Ew | 0x38w => 0x46CAE1D6w
  | 0x39w => 0x2FE28134w | 0x3Aw => 0x5A223942w | 0x3Bw => 0x1863CD5Bw
  | 0x3Cw => 0xC190C6E3w | 0x3Dw => 0x7DFB846w  | 0x3Ew => 0x6EB88816w
  | 0x3Fw => 0x2D0DCC4Aw | 0x40w => 0xA4CCAE59w | 0x41w => 0x3798670Dw
  | 0x42w => 0xCBFA9493w | 0x43w => 0x4F481D45w | 0x44w => 0xEAFC8CA8w
  | 0x45w => 0xDB1129D6w | 0x46w => 0xB0449E20w | 0x47w => 0xF5407FBw
  | 0x48w => 0x6167D9A8w | 0x49w => 0xD1F45763w | 0x4Aw => 0x4DAA96C3w
  | 0x4Bw => 0x3BEC5958w | 0x4Cw => 0xABABA014w | 0x4Dw => 0xB6CCD201w
  | 0x4Ew => 0x38D6279Fw | 0x4Fw => 0x2682215w  | 0x50w => 0x8F376CD5w
  | 0x51w => 0x92C237Ew  | 0x52w => 0xBFC56593w | 0x53w => 0x32889D2Cw
  | 0x54w => 0x854B3E95w | 0x55w => 0x5BB9B43w  | 0x56w => 0x7DCD5DCDw
  | 0x57w => 0xA02E926Cw | 0x58w => 0xFAE527E5w | 0x59w => 0x36A1C330w
  | 0x5Aw => 0x3412E1AEw | 0x5Bw => 0xF257F462w | 0x5Cw => 0x3C4F1D71w
  | 0x5Dw => 0x30A2E809w | 0x5Ew => 0x68E5F551w | 0x5Fw => 0x9C61BA44w
  | 0x60w => 0x5DED0AB8w | 0x61w => 0x75CE09C8w | 0x62w => 0x9654F93Ew
  | 0x63w => 0x698C0CCAw | 0x64w => 0x243CB3E4w | 0x65w => 0x2B062B97w
  | 0x66w => 0xF3B8D9Ew  | 0x67w => 0xE050DFw   | 0x68w => 0xFC5D6166w
  | 0x69w => 0xE35F9288w | 0x6Aw => 0xC079550Dw | 0x6Bw => 0x591AEE8w
  | 0x6Cw => 0x8E531E74w | 0x6Dw => 0x75FE3578w | 0x6Ew => 0x2F6D829Aw
  | 0x6Fw => 0xF60B21AEw | 0x70w => 0x95E8EB8Dw | 0x71w => 0x6699486Bw
  | 0x72w => 0x901D7D9Bw | 0x73w => 0xFD6D6E31w | 0x74w => 0x1090ACEFw
  | 0x75w => 0xE0670DD8w | 0x76w => 0xDAB2E692w | 0x77w => 0xCD6D4365w
  | 0x78w => 0xE5393514w | 0x79w => 0x3AF345F0w | 0x7Aw => 0x6241FC4Dw
  | 0x7Bw => 0x460DA3A3w | 0x7Cw => 0x7BCF3729w | 0x7Dw => 0x8BF1D1E0w
  | 0x7Ew => 0x14AAC070w | 0x7Fw => 0x1587ED55w | 0x80w => 0x3AFD7D3Ew
  | 0x81w => 0xD2F29E01w | 0x82w => 0x29A9D1F6w | 0x83w => 0xEFB10C53w
  | 0x84w => 0xCF3B870Fw | 0x85w => 0xB414935Cw | 0x86w => 0x664465EDw
  | 0x87w => 0x24ACAC7w  | 0x88w => 0x59A744C1w | 0x89w => 0x1D2936A7w
  | 0x8Aw => 0xDC580AA6w | 0x8Bw => 0xCF574CA8w | 0x8Cw => 0x40A7A10w
  | 0x8Dw => 0x6CD81807w | 0x8Ew => 0x8A98BE4Cw | 0x8Fw => 0xACCEA063w
  | 0x90w => 0xC33E92B5w | 0x91w => 0xD1E0E03Dw | 0x92w => 0xB322517Ew
  | 0x93w => 0x2092BD13w | 0x94w => 0x386B2C4Aw | 0x95w => 0x52E8DD58w
  | 0x96w => 0x58656DFBw | 0x97w => 0x50820371w | 0x98w => 0x41811896w
  | 0x99w => 0xE337EF7Ew | 0x9Aw => 0xD39FB119w | 0x9Bw => 0xC97F0DF6w
  | 0x9Cw => 0x68FEA01Bw | 0x9Dw => 0xA150A6E5w | 0x9Ew => 0x55258962w
  | 0x9Fw => 0xEB6FF41Bw | 0xA0w => 0xD7C9CD7Aw | 0xA1w => 0xA619CD9Ew
  | 0xA2w => 0xBCF09576w | 0xA3w => 0x2672C073w | 0xA4w => 0xF003FB3Cw
  | 0xA5w => 0x4AB7A50Bw | 0xA6w => 0x1484126Aw | 0xA7w => 0x487BA9B1w
  | 0xA8w => 0xA64FC9C6w | 0xA9w => 0xF6957D49w | 0xAAw => 0x38B06A75w
  | 0xABw => 0xDD805FCDw | 0xACw => 0x63D094CFw | 0xADw => 0xF51C999Ew
  | 0xAEw => 0x1AA4D343w | 0xAFw => 0xB8495294w | 0xB0w => 0xCE9F8E99w
  | 0xB1w => 0xBFFCD770w | 0xB2w => 0xC7C275CCw | 0xB3w => 0x378453A7w
  | 0xB4w => 0x7B21BE33w | 0xB5w => 0x397F41BDw | 0xB6w => 0x4E94D131w
  | 0xB7w => 0x92CC1F98w | 0xB8w => 0x5915EA51w | 0xB9w => 0x99F861B7w
  | 0xBAw => 0xC9980A88w | 0xBBw => 0x1D74FD5Fw | 0xBCw => 0xB0A495F8w
  | 0xBDw => 0x614DEED0w | 0xBEw => 0xB5778EEAw | 0xBFw => 0x5941792Dw
  | 0xC0w => 0xFA90C1F8w | 0xC1w => 0x33F824B4w | 0xC2w => 0xC4965372w
  | 0xC3w => 0x3FF6D550w | 0xC4w => 0x4CA5FEC0w | 0xC5w => 0x8630E964w
  | 0xC6w => 0x5B3FBBD6w | 0xC7w => 0x7DA26A48w | 0xC8w => 0xB203231Aw
  | 0xC9w => 0x4297514w  | 0xCAw => 0x2D639306w | 0xCBw => 0x2EB13149w
  | 0xCCw => 0x16A45272w | 0xCDw => 0x532459A0w | 0xCEw => 0x8E5F4872w
  | 0xCFw => 0xF966C7D9w | 0xD0w => 0x7128DC0w  | 0xD1w => 0xD44DB62w
  | 0xD2w => 0xAFC8D52Dw | 0xD3w => 0x6316131w  | 0xD4w => 0xD838E7CEw
  | 0xD5w => 0x1BC41D00w | 0xD6w => 0x3A2E8C0Fw | 0xD7w => 0xEA83837Ew
  | 0xD8w => 0xB984737Dw | 0xD9w => 0x13BA4891w | 0xDAw => 0xC4F8B949w
  | 0xDBw => 0xA6D6ACB3w | 0xDCw => 0xA215CDCEw | 0xDDw => 0x8359838Bw
  | 0xDEw => 0x6BD1AA31w | 0xDFw => 0xF579DD52w | 0xE0w => 0x21B93F93w
  | 0xE1w => 0xF5176781w | 0xE2w => 0x187DFDDEw | 0xE3w => 0xE94AEB76w
  | 0xE4w => 0x2B38FD54w | 0xE5w => 0x431DE1DAw | 0xE6w => 0xAB394825w
  | 0xE7w => 0x9AD3048Fw | 0xE8w => 0xDFEA32AAw | 0xE9w => 0x659473E3w
  | 0xEAw => 0x623F7863w | 0xEBw => 0xF3346C59w | 0xECw => 0xAB3AB685w
  | 0xEDw => 0x3346A90Bw | 0xEEw => 0x6B56443Ew | 0xEFw => 0xC6DE01F8w
  | 0xF0w => 0x8D421FC0w | 0xF1w => 0x9B0ED10Cw | 0xF2w => 0x88F1A1E9w
  | 0xF3w => 0x54C1F029w | 0xF4w => 0x7DEAD57Bw | 0xF5w => 0x8D7BA426w
  | 0xF6w => 0x4CF5178Aw | 0xF7w => 0x551A7CCAw | 0xF8w => 0x1A9A5F08w
  | 0xF9w => 0xFCD651B9w | 0xFAw => 0x25605182w | 0xFBw => 0xE11FC6C3w
  | 0xFCw => 0xB6FD9676w | 0xFDw => 0x337B3027w | 0xFEw => 0xB7C8EB14w
  | 0xFFw => 0x9E5FD030w | 0x100w => 0x6B57E354w | 0x101w => 0xAD913CF7w
  | 0x102w => 0x7E16688Dw | 0x103w => 0x58872A69w | 0x104w => 0x2C2FC7DFw
  | 0x105w => 0xE389CCC6w | 0x106w => 0x30738DF1w | 0x107w => 0x824A734w
  | 0x108w => 0xE1797A8Bw | 0x109w => 0xA4A8D57Bw | 0x10Aw => 0x5B5D193Bw
  | 0x10Bw => 0xC8A8309Bw | 0x10Cw => 0x73F9A978w | 0x10Dw => 0x73398D32w
  | 0x10Ew => 0xF59573Ew  | 0x10Fw => 0xE9DF2B03w | 0x110w => 0xE8A5B6C8w
  | 0x111w => 0x848D0704w | 0x112w => 0x98DF93C2w | 0x113w => 0x720A1DC3w
  | 0x114w => 0x684F259Aw | 0x115w => 0x943BA848w | 0x116w => 0xA6370152w
  | 0x117w => 0x863B5EA3w | 0x118w => 0xD17B978Bw | 0x119w => 0x6D9B58EFw
  | 0x11Aw => 0xA700DD4w  | 0x11Bw => 0xA73D36BFw | 0x11Cw => 0x8E6A0829w
  | 0x11Dw => 0x8695BC14w | 0x11Ew => 0xE35B3447w | 0x11Fw => 0x933AC568w
  | 0x120w => 0x8894B022w | 0x121w => 0x2F511C27w | 0x122w => 0xDDFBCC3Cw
  | 0x123w => 0x6662B6w   | 0x124w => 0x117C83FEw | 0x125w => 0x4E12B414w
  | 0x126w => 0xC2BCA766w | 0x127w => 0x3A2FEC10w | 0x128w => 0xF4562420w
  | 0x129w => 0x55792E2Aw | 0x12Aw => 0x46F5D857w | 0x12Bw => 0xCEDA25CEw
  | 0x12Cw => 0xC3601D3Bw | 0x12Dw => 0x6C00AB46w | 0x12Ew => 0xEFAC9C28w
  | 0x12Fw => 0xB3C35047w | 0x130w => 0x611DFEE3w | 0x131w => 0x257C3207w
  | 0x132w => 0xFDD58482w | 0x133w => 0x3B14D84Fw | 0x134w => 0x23BECB64w
  | 0x135w => 0xA075F3A3w | 0x136w => 0x88F8EADw  | 0x137w => 0x7ADF158w
  | 0x138w => 0x7796943Cw | 0x139w => 0xFACABF3Dw | 0x13Aw => 0xC09730CDw
  | 0x13Bw => 0xF7679969w | 0x13Cw => 0xDA44E9EDw | 0x13Dw => 0x2C854C12w
  | 0x13Ew => 0x35935FA3w | 0x13Fw => 0x2F057D9Fw | 0x140w => 0x690624F8w
  | 0x141w => 0x1CB0BAFDw | 0x142w => 0x7B0DBDC6w | 0x143w => 0x810F23BBw
  | 0x144w => 0xFA929A1Aw | 0x145w => 0x6D969A17w | 0x146w => 0x6742979Bw
  | 0x147w => 0x74AC7D05w | 0x148w => 0x10E65C4w  | 0x149w => 0x86A3D963w
  | 0x14Aw => 0xF907B5A0w | 0x14Bw => 0xD0042BD3w | 0x14Cw => 0x158D7D03w
  | 0x14Dw => 0x287A8255w | 0x14Ew => 0xBBA8366Fw | 0x14Fw => 0x96EDC33w
  | 0x150w => 0x21916A7Bw | 0x151w => 0x77B56B86w | 0x152w => 0x951622F9w
  | 0x153w => 0xA6C5E650w | 0x154w => 0x8CEA17D1w | 0x155w => 0xCD8C62BCw
  | 0x156w => 0xA3D63433w | 0x157w => 0x358A68FDw | 0x158w => 0xF9B9D3Cw
  | 0x159w => 0xD6AA295Bw | 0x15Aw => 0xFE33384Aw | 0x15Bw => 0xC000738Ew
  | 0x15Cw => 0xCD67EB2Fw | 0x15Dw => 0xE2EB6DC2w | 0x15Ew => 0x97338B02w
  | 0x15Fw => 0x6C9F246w  | 0x160w => 0x419CF1ADw | 0x161w => 0x2B83C045w
  | 0x162w => 0x3723F18Aw | 0x163w => 0xCB5B3089w | 0x164w => 0x160BEAD7w
  | 0x165w => 0x5D494656w | 0x166w => 0x35F8A74Bw | 0x167w => 0x1E4E6C9Ew
  | 0x168w => 0x399BDw    | 0x169w => 0x67466880w | 0x16Aw => 0xB4174831w
  | 0x16Bw => 0xACF423B2w | 0x16Cw => 0xCA815AB3w | 0x16Dw => 0x5A6395E7w
  | 0x16Ew => 0x302A67C5w | 0x16Fw => 0x8BDB446Bw | 0x170w => 0x108F8FA4w
  | 0x171w => 0x10223EDAw | 0x172w => 0x92B8B48Bw | 0x173w => 0x7F38D0EEw
  | 0x174w => 0xAB2701D4w | 0x175w => 0x262D415w  | 0x176w => 0xAF224A30w
  | 0x177w => 0xB3D88ABAw | 0x178w => 0xF8B2C3AFw | 0x179w => 0xDAF7EF70w
  | 0x17Aw => 0xCC97D3B7w | 0x17Bw => 0xE9614B6Cw | 0x17Cw => 0x2BAEBFF4w
  | 0x17Dw => 0x70F687CFw | 0x17Ew => 0x386C9156w | 0x17Fw => 0xCE092EE5w
  | 0x180w => 0x1E87DA6w  | 0x181w => 0x6CE91E6Aw | 0x182w => 0xBB7BCC84w
  | 0x183w => 0xC7922C20w | 0x184w => 0x9D3B71FDw | 0x185w => 0x60E41C6w
  | 0x186w => 0xD7590F15w | 0x187w => 0x4E03BB47w | 0x188w => 0x183C198Ew
  | 0x189w => 0x63EEB240w | 0x18Aw => 0x2DDBF49Aw | 0x18Bw => 0x6D5CBA54w
  | 0x18Cw => 0x923750AFw | 0x18Dw => 0xF9E14236w | 0x18Ew => 0x7838162Bw
  | 0x18Fw => 0x59726C72w | 0x190w => 0x81B66760w | 0x191w => 0xBB2926C1w
  | 0x192w => 0x48A0CE0Dw | 0x193w => 0xA6C0496Dw | 0x194w => 0xAD43507Bw
  | 0x195w => 0x718D496Aw | 0x196w => 0x9DF057AFw | 0x197w => 0x44B1BDE6w
  | 0x198w => 0x54356DCw  | 0x199w => 0xDE7CED35w | 0x19Aw => 0xD51A138Bw
  | 0x19Bw => 0x62088CC9w | 0x19Cw => 0x35830311w | 0x19Dw => 0xC96EFCA2w
  | 0x19Ew => 0x686F86ECw | 0x19Fw => 0x8E77CB68w | 0x1A0w => 0x63E1D6B8w
  | 0x1A1w => 0xC80F9778w | 0x1A2w => 0x79C491FDw | 0x1A3w => 0x1B4C67F2w
  | 0x1A4w => 0x72698D7Dw | 0x1A5w => 0x5E368C31w | 0x1A6w => 0xF7D95E2Ew
  | 0x1A7w => 0xA1D3493Fw | 0x1A8w => 0xDCD9433Ew | 0x1A9w => 0x896F1552w
  | 0x1AAw => 0x4BC4CA7Aw | 0x1ABw => 0xA6D1BAF4w | 0x1ACw => 0xA5A96DCCw
  | 0x1ADw => 0xBEF8B46w  | 0x1AEw => 0xA169FDA7w | 0x1AFw => 0x74DF40B7w
  | 0x1B0w => 0x4E208804w | 0x1B1w => 0x9A756607w | 0x1B2w => 0x38E87C8w
  | 0x1B3w => 0x20211E44w | 0x1B4w => 0x8B7AD4BFw | 0x1B5w => 0xC6403F35w
  | 0x1B6w => 0x1848E36Dw | 0x1B7w => 0x80BDB038w | 0x1B8w => 0x1E62891Cw
  | 0x1B9w => 0x643D2107w | 0x1BAw => 0xBF04D6F8w | 0x1BBw => 0x21092C8Cw
  | 0x1BCw => 0xF644F389w | 0x1BDw => 0x778404Ew  | 0x1BEw => 0x7B78ADB8w
  | 0x1BFw => 0xA2C52D53w | 0x1C0w => 0x42157ABEw | 0x1C1w => 0xA2253E2Ew
  | 0x1C2w => 0x7BF3F4AEw | 0x1C3w => 0x80F594F9w | 0x1C4w => 0x953194E7w
  | 0x1C5w => 0x77EB92EDw | 0x1C6w => 0xB3816930w | 0x1C7w => 0xDA8D9336w
  | 0x1C8w => 0xBF447469w | 0x1C9w => 0xF26D9483w | 0x1CAw => 0xEE6FAED5w
  | 0x1CBw => 0x71371235w | 0x1CCw => 0xDE425F73w | 0x1CDw => 0xB4E59F43w
  | 0x1CEw => 0x7DBE2D4Ew | 0x1CFw => 0x2D37B185w | 0x1D0w => 0x49DC9A63w
  | 0x1D1w => 0x98C39D98w | 0x1D2w => 0x1301C9A2w | 0x1D3w => 0x389B1BBFw
  | 0x1D4w => 0xC18588Dw  | 0x1D5w => 0xA421C1BAw | 0x1D6w => 0x7AA3865Cw
  | 0x1D7w => 0x71E08558w | 0x1D8w => 0x3C5CFCAAw | 0x1D9w => 0x7D239CA4w
  | 0x1DAw => 0x297D9DDw  | 0x1DBw => 0xD7DC2830w | 0x1DCw => 0x4B37802Bw
  | 0x1DDw => 0x7428AB54w | 0x1DEw => 0xAEEE0347w | 0x1DFw => 0x4B3FBB85w
  | 0x1E0w => 0x692F2F08w | 0x1E1w => 0x134E578Ew | 0x1E2w => 0x36D9E0BFw
  | 0x1E3w => 0xAE8B5FCFw | 0x1E4w => 0xEDB93ECFw | 0x1E5w => 0x2B27248Ew
  | 0x1E6w => 0x170EB1EFw | 0x1E7w => 0x7DC57FD6w | 0x1E8w => 0x1E760F16w
  | 0x1E9w => 0xB1136601w | 0x1EAw => 0x864E1B9Bw | 0x1EBw => 0xD7EA7319w
  | 0x1ECw => 0x3AB871BDw | 0x1EDw => 0xCFA4D76Fw | 0x1EEw => 0xE31BD782w
  | 0x1EFw => 0xDBEB469w  | 0x1F0w => 0xABB96061w | 0x1F1w => 0x5370F85Dw
  | 0x1F2w => 0xFFB07E37w | 0x1F3w => 0xDA30D0FBw | 0x1F4w => 0xEBC977B6w
  | 0x1F5w => 0xB98B40Fw  | 0x1F6w => 0x3A4D0FE6w | 0x1F7w => 0xDF4FC26Bw
  | 0x1F8w => 0x159CF22Aw | 0x1F9w => 0xC298D6E2w | 0x1FAw => 0x2B78EF6Aw
  | 0x1FBw => 0x61A94AC0w | 0x1FCw => 0xAB561187w | 0x1FDw => 0x14EEA0F0w
  | 0x1FEw => 0xDF0D4164w | 0x1FFw => 0x19AF70EEw`;

val Sbox0_def = Define `
  Sbox0 i = Sbox i`;

val Sbox1_def = Define `
  Sbox1 i = Sbox (i+0xffw)`;

val _ = export_theory();
